Extend certified first-crossing descent to 2592 and classify feasible times - #4

A first coefficient contraction does not by itself guarantee integer descent. This change extends the certified crossing-to-descent horizon from 1,538 to 2,592 for every n>1, and isolates the remaining unbounded descent condition as a proposition equivalent to Collatz.

It also classifies possible coefficient first-crossing times at every depth by occupied power bands, constructs arbitrarily large realizing inputs, and transfers that classification to actual stopping through 2,592. The depth-fifteen atlas proves four infinite-class statements for each of 32,768 residues; 173 classes stop first at fifteen, with a certified rational density and finite discrepancy bound.

The Collatz conjecture remains unproved. ResidualCoverage and the stronger sufficient ResidualGapCoverage are explicit open conditions, not assumed axioms. Research notes identify the next arithmetic obstruction and qualify the cited literature, including corrections and withdrawn work.

CI now explicitly builds Collatz before saving the Lake cache, so the integrity step can reuse a complete library build.

Validation:

• Full library build and repository integrity passed (4,524 build jobs).
• 131,850 new named theorems audited; only standard logical axioms observed.
• 2,651,669 independent checks passed; six false certificate controls rejected.
• 370,311 new Lean code lines excluding comments, blank lines and the audit driver.
• 1,000 distinct new certificate commits verified against historical source hashes.

The large volume is predominantly generated proof-carrying data, not 1,000 independent discoveries. Merge without squashing to preserve the audited commit identities; remove the temporary research branch afterward. See Research/PassageAtlas/README.md and verification.json for reproducible statements, evidence, and limits.